#include <forward_list>
#include <fstream>
#include <cstring>
#include <cassert>
#include <future>
#include <limits>
#include <memory>
#include <optional>
#include <queue>
#include <type_traits>
#include <vector>
#include <array>
#include <bitset>
#include <algorithm>
#include <iostream>
#include <iomanip>
#include <chrono>

#define len(clause) (clause.ref.count()) 

#define  caRESET       "\e[0m"
#define  caBOLD        "\e[1m"
#define  fgBLACK       "\e[30m"
#define  fgRED         "\e[31m"
#define  fgGREEN       "\e[32m"
#define  fgBLUE        "\e[34m"
#define  fgLIGHTRED    "\e[91m"
#define  bgGRAY        "\e[47m"
#define  bgDARKGRAY    "\e[100m"

typedef std::chrono::high_resolution_clock Clock;

// ==================================================================
// Helper functions for parsing DIMACS CNF.

char *readWS(char *p) {
  while (1) switch(*p) {
    default: return p;
    case 9 ... 13: case 32: ++p;
  }
}

char *readNL(char *p) {
  while (*p != '\n') if (*p++ == '\0') exit(1);
  return ++p;
}

char *readNum(char *p, int *i) {
  int sgn = 1; *i = 0;
  p = readWS(p);
  while(1) switch(*p) {
    case 0        : return p;
    case '-'      : sgn = -1; ++p; break;
    case '0'...'9': *i = *i * 10 + (*p - '0'); ++p; break;
    default: goto done;
  }

done:
  *i *= sgn;
  return p;
}
// ==================================================================

const int VAR_NUM = 256;

typedef std::bitset<VAR_NUM> BitSeq;

typedef int32_t Lit;
typedef Lit VarSeq[VAR_NUM];
typedef double VarScr[VAR_NUM];

class Clause {
  public:
  BitSeq ref, pol;

  void rst(){
    ref.reset();
    pol.reset();
  }

  void set(Lit l) {
    assert(l != 0);
    ref[abs(l)] = 1;
    pol[abs(l)] = l > 0;
  } 

  void clr(Lit l) {
    ref[abs(l)] = 0;
    pol[abs(l)] = 0;
  }

  void print(int varRange) {
    for (int i = 1; i < varRange; i++)
      if (!ref[i])
        std::cout << bgDARKGRAY " " caRESET;
      else if (pol[i])
        std::cout << bgDARKGRAY caBOLD fgBLACK << "+" caRESET; 
      else 
        std::cout << bgDARKGRAY caBOLD fgBLACK << "-" caRESET;
    std::cout << "\n";
  }
};

typedef std::optional<Clause> ClauOp;

typedef struct ProLit {
  Lit dex;
  int lev;
  ClauOp ant;
} ProLit;

typedef std::vector<Clause> LitMem;

class Solver {
public:
    Clause              learnt;
    LitMem              litMem;                 // clause storage
    int varNum, claNum;                         // number of variables and clauses

                                                // Be advised that the naming follows the convention of 
                                                // VeriSAT, instead of orignal EasySAT, for convenience
                                                // of translating to Verilog later.

    Clause valMem;                              // The variable assignement () 
                                                // valMem.ref[i] == 0: unassigned
                                                // valMem.ref[i] == 1: assigned, 
                                                // with sign of (valMem.pol[i] ? 1 : -1)

    VarSeq decLev;                              // variables' decision level
    VarSeq decPos;                              // locations of branching variables in the trail
    int    decLen;                              // the length of decPos / the number of assigned variables
                                                // also indicates the current decision level

    std::array<ProLit, VAR_NUM> proMem;                              // The trail (stack of assigned variable via both decision & 
                                                // propagation)
    // std::array<ClauOp, VAR_NUM> reason;         // the clause causing the assignment. Note that this
                                                // is associated with the trail,
    int    proLen;                              // number of all assigned variables (literals).
    int    proTop;                              // number of propagted literals
    int    proCnt;
     
    int    varInc;
    VarScr varScr;


    int val(Clause& c, Lit& res);
    void alloc();                                      // initialize vars & alloc mem. 
    void assign(int lit, int level, ClauOp c);          // assign a variable.
    ClauOp  prop();                                       // BCP
    void back(int bakLev);                             // Backtracking
    int  conf(Clause& c);   // Conflict analysis.
    int  parse(char *filename);                        // Parsing DIMACS CNF.
    int  solve();                                      // Main solving procedure.
    int  fork();                                       // select a branching variable.
    void addClause(Clause &c);                         // add new clause to clause storage.
    void printModel();                                 // print the model when resulting SAT.

    void bumpCl(double inc, Clause &c);
    void decay(double coeff);
};

void Solver::addClause(Clause &c) {
    Clause r = c;
    litMem.push_back(r);
}

void Solver::bumpCl(double inc, Clause &c) {
  for (int i = 0; i < VAR_NUM; i++) if (c.ref[i]) varScr[i] += inc; 
}

void Solver::decay(double coeff) {
  for (int i = 0; i < VAR_NUM; i++) varScr[i] *= coeff; 
}

int Solver::val(Clause &c, Lit& res) {

  Clause valMem;

  for(int i = 0; i < proLen; i++)
    valMem.set(proMem[i].dex);

  if ((c.ref & valMem.ref & ~(c.pol ^ valMem.pol)).any()) // if variable occurs in the clause, assigned, and has
    return 1;                                             // same sign (NXOR to be true), then clause rectified.

  auto uniMask = c.ref & ~valMem.ref;                     // if variable occurs but not assigned, then count the
  for (int i = 0; i < VAR_NUM; i++)                       // number. Zero means all variables assigned and clause
    if (uniMask[i]) res = i * (c.pol[i] ? 1 : -1);        // falsified. Only one implies it's a unit clause.
    
  return -uniMask.count();
}

int Solver::parse(char *filename) {

  std::ifstream fin(filename);
  fin.seekg(0, fin.end);
  size_t fileSize = fin.tellg();
	fin.seekg(0, fin.beg);
	char *data = new char[fileSize + 1], *p = data;
	fin.read(data, fileSize);
	fin.close();

	data[fileSize] = '\0';
  Clause buf;
  while (1) {
    p = readWS(p);
    switch(*p) {
      case '%' : // special handling for SATLIB benchmarks 
      case '\0': goto doneParse;
      case 'c' : p = readNL(p); break;
      case 'p' : if (!memcmp(p, "p cnf", 5)) {
                   p += 5, p = readNum(p, &varNum), p = readNum(p, &claNum);
                   alloc();
                 }
                 break;
      default  : Lit lit, res = 0;
                 p = readNum(p, &lit);
                 if (*p == '\0' && lit != 0)
                   printf("c PARSE ERROR! Unexpected EOF\n"), exit(1);
                 if (lit == 0) {
                   switch(len(buf)) {
                     case 0: return 20;
                     case 1: switch(val(buf, res)) {
                               case  0: return 20;
                               case -1: assign(res, 0, std::nullopt);
                             }
                     default: addClause(buf);
                   }
                   buf.rst();
                 }
                 else buf.set(lit);
    }
  }

doneParse:

  return (prop() != std::nullopt) ? 20 : 0;
}

void Solver::alloc() {
  memset(decLev,  -1, VAR_NUM * sizeof(*decLev));
  memset(decPos,  0, VAR_NUM * sizeof(*decPos));
  memset(varScr,  0, VAR_NUM * sizeof(*varScr));

  // for first comparison
  varScr[0] = -std::numeric_limits<double>::max();

  for (int i = 0; i < VAR_NUM; i++) {
    proMem[i].lev = 0;
    proMem[i].dex = 0;
    proMem[i].ant = std::nullopt;

  }

  proLen = 0;
  proTop = 0;
  decLen = 0;

  proCnt = 0;
}

void Solver::assign(int lit, int l, std::optional<Clause> c) {
    int var = abs(lit);
    decLev[var] = l;

    proMem[proLen].lev = l;
    proMem[proLen].dex = lit;
    proMem[proLen].ant = c;
    proLen ++;
}

ClauOp Solver::prop() {
  Lit res;
  while (proTop < proLen) {
    assert(proTop == proLen - 1);
    for(auto& c: litMem) {
      proCnt++;
      switch(val(c, res)) {
        case  1: break;
        case  0: return c;
        case -1: assign(res, proMem[proTop].lev, c);
                 goto breakLoop;
        default:; 
      }
      continue;
breakLoop:
      break;
    }

    proTop++;
  }
  return std::nullopt;
}

int Solver::conf(Clause& con) {

  learnt.rst();
  if (proMem[proTop].lev == 0) return 20;

  // assert(decLen == proMem[proTop].lev);
  int bakPtr = proLen - 1;

  learnt.ref = con.ref;
  learnt.pol = con.pol;

  std::bitset<VAR_NUM> equDecLen;
  for (int i = 0; i < proLen; i++)
    equDecLen[abs(proMem[i].dex)] = proMem[i].lev == proMem[proTop].lev;

  while(1) {

    if (proMem[bakPtr].ant == std::nullopt) {
      assert((learnt.ref & equDecLen).count() == 1);
    }
    
    if ((learnt.ref & equDecLen).count() == 1) break;       // coundition of finding 1st UIP
    auto reazon = proMem[bakPtr].ant.value();                   // next clause on the reason stack

    auto resMask = 
      learnt.ref & reazon.ref & (learnt.pol ^ reazon.pol);  // condition of resolution

    if(resMask.any()) {
      learnt.ref = (learnt.ref | reazon.ref) & ~resMask;
      learnt.pol = (learnt.pol | reazon.pol) & ~resMask;
    }

    bakPtr--;
    assert(bakPtr >= 0);
  }

  // bakLev
  int bakLev = 0;
  auto bakLevPos = learnt.ref & ~equDecLen;
  if(len(learnt) > 1) 
    for (int i = 0; i < VAR_NUM; i++) 
      if (bakLevPos[i])
        bakLev = decLev[i] > bakLev ? decLev[i] : bakLev;


  // determinnig resLit
  int resLit = 0;
  auto resLitPos = learnt.ref & equDecLen;
  while(!resLitPos[abs(proMem[bakPtr].dex)] && bakPtr > -1) bakPtr--;
  resLit = -proMem[bakPtr].dex;

  // while(proMem[bakPtr-1].lev >= proMem[proTop].lev && bakPtr > -1) bakPtr--;
  if (len(learnt) > 1) {
    while(!bakLevPos[abs(proMem[bakPtr].dex)] && bakPtr > -1) bakPtr--;
    assert(bakLevPos[abs(proMem[bakPtr].dex)]);
    assert(proMem[bakPtr].lev == bakLev);
    // bakLev = proMem[bakPtr].lev;
  }

  // for(int i = 0; i < proLen; i++) 
  //   if (i == bakPtr)
  //     std::cout << fgRED << std::setw(4)<< proMem[i].dex << "@" << proMem[i].lev << caRESET << " ";
  //   else if (i == decPos[proMem[bakPtr].lev])
  //     std::cout << fgBLUE << std::setw(4)<< proMem[i].dex << "@" << proMem[i].lev << caRESET << " ";
  //   else
  //     std::cout << std::setw(4)<< proMem[i].dex << "@" << proMem[i].lev << " ";
  // std::cout << "\n";
  // std::cout << "DES " << decPos[bakLev] << " " << bakPtr << "\n";

  proTop = decPos[bakLev];
  proLen = proTop;
  decLen = bakLev;

  if (len(learnt) == 1) assign(resLit, 0, std::nullopt);
  else {
    addClause(learnt);
    assign(resLit, bakLev, learnt);
  }

  // for (int i = proLen; i >= 0; i--)
  //   if (proMem[i].dex == resLit) {
  //     std::cout << proMem[i].dex << std::setw(5) << proMem[i].lev << (proMem[i].ant == std::nullopt) << "\n";
  //   }
      

  // bakLev = decPos[bakLev]; 
  // assert(bakPtr >= decPos[bakLev]);

  // bakPtr = proLen;
  // auto bakLevPos2 = learnt.ref & ~equDecLen;
  // while(!bakLevPos2[abs(proMem[bakPtr].dex)] && bakPtr > 0) {
  //   bakPtr --;
  // }

  // std::cout <<bakLevPos2 << "\n";
    
  // while(proMem[bakPtr].ant != std::nullopt) bakPtr--;
  // bakPtr--;

  // std::cout << std::setw(4)  <<bakPtr << " " << std::setw(4) <<  decPos[bakLev] << " |";

  //   for(int i = 0; i < proLen; i++) 
  //     if (i == bakPtr)
  //       std::cout << fgRED << std::setw(4)<< proMem[i].dex << "@" << proMem[i].lev << caRESET << " ";
  //     else if (i == decPos[bakLev])
  //       std::cout << fgBLUE << std::setw(4)<< proMem[i].dex << "@" << proMem[i].lev << caRESET << " ";
  //     else
  //       std::cout << std::setw(4)<< proMem[i].dex << "@" << proMem[i].lev << " ";
  //   std::cout << "\n";


  // assert(bakPtr == decPos[bakLev]);


  return 0;
}

void Solver::back(int bakLev) {
  // assert(decLen > bakLev);
}

int Solver::fork() {

  Clause valMem;
  for(int i = 0; i < proLen; i++)
    valMem.set(proMem[i].dex);

  int next = 0;

  for (int i = 1; i < varNum + 1; i++) {
    if((varScr[next] < varScr[i]) && (valMem.ref[i] == 0))
      next = i;
  }

  if (next > 0) {
    decPos[decLen] = proLen;
    decLen ++;
    assign(next, proMem[proTop-1].lev + 1, std::nullopt);
    return 0;
  } else {
    return 10;
  }

}

int Solver::solve() {
  int res = 0;
  while (!res) {
    auto con = prop();
    if (con != std::nullopt) {
      bumpCl(1, con.value());
      res = conf(con.value());
      if (res == 20) break;
      decay(0.95);

    }
    else res = fork();
  }
  return res;
}

void Solver::printModel() {
    printf("v ");
    for (int i = 1; i <= varNum; i++) printf("%d ", (valMem.pol[i] ? 1 : -1) * i);
    puts("0");
}

int main(int argc, char **argv) {
    Solver S;
    auto beg = Clock::now();
    std::cout << "c FILE           " caBOLD << std::setw(20) << argv[1] << caRESET "\n";
    int res = S.parse(argv[1]);
    auto mid = Clock::now();
    std::cout << "c elapse::parsing" caBOLD fgBLUE << std::setw(20) << std::chrono::duration_cast<std::chrono::microseconds>(mid - beg).count() << "(us)" caRESET "\n";
    if (res == 20) printf("c parsing stage caused\ns UNSATISFIABLE\n");
    else {
        res = S.solve();
        auto fin = Clock::now();
        std::cout << "c elapse::solving" caBOLD fgBLUE << std::setw(20) << std::chrono::duration_cast<std::chrono::microseconds>(fin - mid).count() << "(us)" caRESET "\n";
        std::cout << "c PROP COUNT:    " caBOLD fgLIGHTRED << std::setw(20) <<  S.proCnt << caRESET "\n";
        if (res == 10) {
            std::cout << "s " caBOLD fgGREEN "SATISFIABLE" caRESET "\n";
            S.printModel();
        }
        else if (res == 20) 
            std::cout << "s " caBOLD fgRED "UNSATISFIABLE" caRESET "\n";
    }
    return 0;
}
